Problem:
 __(__(X,Y),Z) -> __(X,__(Y,Z))
 __(X,nil()) -> X
 __(nil(),X) -> X
 U11(tt()) -> tt()
 U21(tt(),V2) -> U22(isList(activate(V2)))
 U22(tt()) -> tt()
 U31(tt()) -> tt()
 U41(tt(),V2) -> U42(isNeList(activate(V2)))
 U42(tt()) -> tt()
 U51(tt(),V2) -> U52(isList(activate(V2)))
 U52(tt()) -> tt()
 U61(tt()) -> tt()
 U71(tt(),P) -> U72(isPal(activate(P)))
 U72(tt()) -> tt()
 U81(tt()) -> tt()
 isList(V) -> U11(isNeList(activate(V)))
 isList(n__nil()) -> tt()
 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
 isNeList(V) -> U31(isQid(activate(V)))
 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
 isNePal(V) -> U61(isQid(activate(V)))
 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
 isPal(V) -> U81(isNePal(activate(V)))
 isPal(n__nil()) -> tt()
 isQid(n__a()) -> tt()
 isQid(n__e()) -> tt()
 isQid(n__i()) -> tt()
 isQid(n__o()) -> tt()
 isQid(n__u()) -> tt()
 nil() -> n__nil()
 __(X1,X2) -> n____(X1,X2)
 a() -> n__a()
 e() -> n__e()
 i() -> n__i()
 o() -> n__o()
 u() -> n__u()
 activate(n__nil()) -> nil()
 activate(n____(X1,X2)) -> __(X1,X2)
 activate(n__a()) -> a()
 activate(n__e()) -> e()
 activate(n__i()) -> i()
 activate(n__o()) -> o()
 activate(n__u()) -> u()
 activate(X) -> X

Proof:
 Complexity Transformation Processor:
  strict:
   __(__(X,Y),Z) -> __(X,__(Y,Z))
   __(X,nil()) -> X
   __(nil(),X) -> X
   U11(tt()) -> tt()
   U21(tt(),V2) -> U22(isList(activate(V2)))
   U22(tt()) -> tt()
   U31(tt()) -> tt()
   U41(tt(),V2) -> U42(isNeList(activate(V2)))
   U42(tt()) -> tt()
   U51(tt(),V2) -> U52(isList(activate(V2)))
   U52(tt()) -> tt()
   U61(tt()) -> tt()
   U71(tt(),P) -> U72(isPal(activate(P)))
   U72(tt()) -> tt()
   U81(tt()) -> tt()
   isList(V) -> U11(isNeList(activate(V)))
   isList(n__nil()) -> tt()
   isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
   isNeList(V) -> U31(isQid(activate(V)))
   isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
   isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
   isNePal(V) -> U61(isQid(activate(V)))
   isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
   isPal(V) -> U81(isNePal(activate(V)))
   isPal(n__nil()) -> tt()
   isQid(n__a()) -> tt()
   isQid(n__e()) -> tt()
   isQid(n__i()) -> tt()
   isQid(n__o()) -> tt()
   isQid(n__u()) -> tt()
   nil() -> n__nil()
   __(X1,X2) -> n____(X1,X2)
   a() -> n__a()
   e() -> n__e()
   i() -> n__i()
   o() -> n__o()
   u() -> n__u()
   activate(n__nil()) -> nil()
   activate(n____(X1,X2)) -> __(X1,X2)
   activate(n__a()) -> a()
   activate(n__e()) -> e()
   activate(n__i()) -> i()
   activate(n__o()) -> o()
   activate(n__u()) -> u()
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [u] = 0,
     
     [o] = 0,
     
     [i] = 0,
     
     [e] = 0,
     
     [a] = 0,
     
     [n__u] = 0,
     
     [n__o] = 0,
     
     [n__i] = 8,
     
     [n__e] = 3,
     
     [n__a] = 0,
     
     [isNePal](x0) = x0 + 10,
     
     [isQid](x0) = x0 + 13,
     
     [n____](x0, x1) = x0 + x1,
     
     [n__nil] = 8,
     
     [U81](x0) = x0 + 12,
     
     [U72](x0) = x0 + 12,
     
     [isPal](x0) = x0 + 2,
     
     [U71](x0, x1) = x0 + x1 + 6,
     
     [U61](x0) = x0 + 7,
     
     [U52](x0) = x0 + 4,
     
     [U51](x0, x1) = x0 + x1 + 9,
     
     [U42](x0) = x0 + 4,
     
     [isNeList](x0) = x0 + 10,
     
     [U41](x0, x1) = x0 + x1 + 7,
     
     [U31](x0) = x0 + 6,
     
     [U22](x0) = x0 + 2,
     
     [isList](x0) = x0 + 5,
     
     [activate](x0) = x0 + 5,
     
     [U21](x0, x1) = x0 + x1 + 6,
     
     [U11](x0) = x0 + 8,
     
     [tt] = 8,
     
     [nil] = 4,
     
     [__](x0, x1) = x0 + x1 + 10
    orientation:
     __(__(X,Y),Z) = X + Y + Z + 20 >= X + Y + Z + 20 = __(X,__(Y,Z))
     
     __(X,nil()) = X + 14 >= X = X
     
     __(nil(),X) = X + 14 >= X = X
     
     U11(tt()) = 16 >= 8 = tt()
     
     U21(tt(),V2) = V2 + 14 >= V2 + 12 = U22(isList(activate(V2)))
     
     U22(tt()) = 10 >= 8 = tt()
     
     U31(tt()) = 14 >= 8 = tt()
     
     U41(tt(),V2) = V2 + 15 >= V2 + 19 = U42(isNeList(activate(V2)))
     
     U42(tt()) = 12 >= 8 = tt()
     
     U51(tt(),V2) = V2 + 17 >= V2 + 14 = U52(isList(activate(V2)))
     
     U52(tt()) = 12 >= 8 = tt()
     
     U61(tt()) = 15 >= 8 = tt()
     
     U71(tt(),P) = P + 14 >= P + 19 = U72(isPal(activate(P)))
     
     U72(tt()) = 20 >= 8 = tt()
     
     U81(tt()) = 20 >= 8 = tt()
     
     isList(V) = V + 5 >= V + 23 = U11(isNeList(activate(V)))
     
     isList(n__nil()) = 13 >= 8 = tt()
     
     isList(n____(V1,V2)) = V1 + V2 + 5 >= V1 + V2 + 21 = U21(isList(activate(V1)),activate(V2))
     
     isNeList(V) = V + 10 >= V + 24 = U31(isQid(activate(V)))
     
     isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 22 = U41(isList(activate(V1)),activate(V2))
     
     isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 29 = U51(isNeList(activate(V1)),activate(V2))
     
     isNePal(V) = V + 10 >= V + 25 = U61(isQid(activate(V)))
     
     isNePal(n____(I,__(P,I))) = 2I + P + 20 >= I + P + 29 = U71(isQid(activate(I)),activate(P))
     
     isPal(V) = V + 2 >= V + 27 = U81(isNePal(activate(V)))
     
     isPal(n__nil()) = 10 >= 8 = tt()
     
     isQid(n__a()) = 13 >= 8 = tt()
     
     isQid(n__e()) = 16 >= 8 = tt()
     
     isQid(n__i()) = 21 >= 8 = tt()
     
     isQid(n__o()) = 13 >= 8 = tt()
     
     isQid(n__u()) = 13 >= 8 = tt()
     
     nil() = 4 >= 8 = n__nil()
     
     __(X1,X2) = X1 + X2 + 10 >= X1 + X2 = n____(X1,X2)
     
     a() = 0 >= 0 = n__a()
     
     e() = 0 >= 3 = n__e()
     
     i() = 0 >= 8 = n__i()
     
     o() = 0 >= 0 = n__o()
     
     u() = 0 >= 0 = n__u()
     
     activate(n__nil()) = 13 >= 4 = nil()
     
     activate(n____(X1,X2)) = X1 + X2 + 5 >= X1 + X2 + 10 = __(X1,X2)
     
     activate(n__a()) = 5 >= 0 = a()
     
     activate(n__e()) = 8 >= 0 = e()
     
     activate(n__i()) = 13 >= 0 = i()
     
     activate(n__o()) = 5 >= 0 = o()
     
     activate(n__u()) = 5 >= 0 = u()
     
     activate(X) = X + 5 >= X = X
    problem:
     strict:
      __(__(X,Y),Z) -> __(X,__(Y,Z))
      U41(tt(),V2) -> U42(isNeList(activate(V2)))
      U71(tt(),P) -> U72(isPal(activate(P)))
      isList(V) -> U11(isNeList(activate(V)))
      isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
      isNeList(V) -> U31(isQid(activate(V)))
      isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
      isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
      isNePal(V) -> U61(isQid(activate(V)))
      isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
      isPal(V) -> U81(isNePal(activate(V)))
      nil() -> n__nil()
      a() -> n__a()
      e() -> n__e()
      i() -> n__i()
      o() -> n__o()
      u() -> n__u()
      activate(n____(X1,X2)) -> __(X1,X2)
     weak:
      __(X,nil()) -> X
      __(nil(),X) -> X
      U11(tt()) -> tt()
      U21(tt(),V2) -> U22(isList(activate(V2)))
      U22(tt()) -> tt()
      U31(tt()) -> tt()
      U42(tt()) -> tt()
      U51(tt(),V2) -> U52(isList(activate(V2)))
      U52(tt()) -> tt()
      U61(tt()) -> tt()
      U72(tt()) -> tt()
      U81(tt()) -> tt()
      isList(n__nil()) -> tt()
      isPal(n__nil()) -> tt()
      isQid(n__a()) -> tt()
      isQid(n__e()) -> tt()
      isQid(n__i()) -> tt()
      isQid(n__o()) -> tt()
      isQid(n__u()) -> tt()
      __(X1,X2) -> n____(X1,X2)
      activate(n__nil()) -> nil()
      activate(n__a()) -> a()
      activate(n__e()) -> e()
      activate(n__i()) -> i()
      activate(n__o()) -> o()
      activate(n__u()) -> u()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [u] = 10,
       
       [o] = 10,
       
       [i] = 10,
       
       [e] = 10,
       
       [a] = 10,
       
       [n__u] = 2,
       
       [n__o] = 2,
       
       [n__i] = 2,
       
       [n__e] = 2,
       
       [n__a] = 2,
       
       [isNePal](x0) = x0 + 1,
       
       [isQid](x0) = x0 + 5,
       
       [n____](x0, x1) = x0 + x1 + 12,
       
       [n__nil] = 5,
       
       [U81](x0) = x0,
       
       [U72](x0) = x0,
       
       [isPal](x0) = x0 + 2,
       
       [U71](x0, x1) = x0 + x1 + 10,
       
       [U61](x0) = x0,
       
       [U52](x0) = x0,
       
       [U51](x0, x1) = x0 + x1 + 3,
       
       [U42](x0) = x0,
       
       [isNeList](x0) = x0 + 9,
       
       [U41](x0, x1) = x0 + x1,
       
       [U31](x0) = x0,
       
       [U22](x0) = x0,
       
       [isList](x0) = x0 + 2,
       
       [activate](x0) = x0 + 8,
       
       [U21](x0, x1) = x0 + x1 + 3,
       
       [U11](x0) = x0,
       
       [tt] = 7,
       
       [nil] = 13,
       
       [__](x0, x1) = x0 + x1 + 14
      orientation:
       __(__(X,Y),Z) = X + Y + Z + 28 >= X + Y + Z + 28 = __(X,__(Y,Z))
       
       U41(tt(),V2) = V2 + 7 >= V2 + 17 = U42(isNeList(activate(V2)))
       
       U71(tt(),P) = P + 17 >= P + 10 = U72(isPal(activate(P)))
       
       isList(V) = V + 2 >= V + 17 = U11(isNeList(activate(V)))
       
       isList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 21 = U21(isList(activate(V1)),activate(V2))
       
       isNeList(V) = V + 9 >= V + 13 = U31(isQid(activate(V)))
       
       isNeList(n____(V1,V2)) = V1 + V2 + 21 >= V1 + V2 + 18 = U41(isList(activate(V1)),activate(V2))
       
       isNeList(n____(V1,V2)) = V1 + V2 + 21 >= V1 + V2 + 28 = U51(isNeList(activate(V1)),activate(V2))
       
       isNePal(V) = V + 1 >= V + 13 = U61(isQid(activate(V)))
       
       isNePal(n____(I,__(P,I))) = 2I + P + 27 >= I + P + 31 = U71(isQid(activate(I)),activate(P))
       
       isPal(V) = V + 2 >= V + 9 = U81(isNePal(activate(V)))
       
       nil() = 13 >= 5 = n__nil()
       
       a() = 10 >= 2 = n__a()
       
       e() = 10 >= 2 = n__e()
       
       i() = 10 >= 2 = n__i()
       
       o() = 10 >= 2 = n__o()
       
       u() = 10 >= 2 = n__u()
       
       activate(n____(X1,X2)) = X1 + X2 + 20 >= X1 + X2 + 14 = __(X1,X2)
       
       __(X,nil()) = X + 27 >= X = X
       
       __(nil(),X) = X + 27 >= X = X
       
       U11(tt()) = 7 >= 7 = tt()
       
       U21(tt(),V2) = V2 + 10 >= V2 + 10 = U22(isList(activate(V2)))
       
       U22(tt()) = 7 >= 7 = tt()
       
       U31(tt()) = 7 >= 7 = tt()
       
       U42(tt()) = 7 >= 7 = tt()
       
       U51(tt(),V2) = V2 + 10 >= V2 + 10 = U52(isList(activate(V2)))
       
       U52(tt()) = 7 >= 7 = tt()
       
       U61(tt()) = 7 >= 7 = tt()
       
       U72(tt()) = 7 >= 7 = tt()
       
       U81(tt()) = 7 >= 7 = tt()
       
       isList(n__nil()) = 7 >= 7 = tt()
       
       isPal(n__nil()) = 7 >= 7 = tt()
       
       isQid(n__a()) = 7 >= 7 = tt()
       
       isQid(n__e()) = 7 >= 7 = tt()
       
       isQid(n__i()) = 7 >= 7 = tt()
       
       isQid(n__o()) = 7 >= 7 = tt()
       
       isQid(n__u()) = 7 >= 7 = tt()
       
       __(X1,X2) = X1 + X2 + 14 >= X1 + X2 + 12 = n____(X1,X2)
       
       activate(n__nil()) = 13 >= 13 = nil()
       
       activate(n__a()) = 10 >= 10 = a()
       
       activate(n__e()) = 10 >= 10 = e()
       
       activate(n__i()) = 10 >= 10 = i()
       
       activate(n__o()) = 10 >= 10 = o()
       
       activate(n__u()) = 10 >= 10 = u()
       
       activate(X) = X + 8 >= X = X
      problem:
       strict:
        __(__(X,Y),Z) -> __(X,__(Y,Z))
        U41(tt(),V2) -> U42(isNeList(activate(V2)))
        isList(V) -> U11(isNeList(activate(V)))
        isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
        isNeList(V) -> U31(isQid(activate(V)))
        isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
        isNePal(V) -> U61(isQid(activate(V)))
        isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
        isPal(V) -> U81(isNePal(activate(V)))
       weak:
        U71(tt(),P) -> U72(isPal(activate(P)))
        isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
        nil() -> n__nil()
        a() -> n__a()
        e() -> n__e()
        i() -> n__i()
        o() -> n__o()
        u() -> n__u()
        activate(n____(X1,X2)) -> __(X1,X2)
        __(X,nil()) -> X
        __(nil(),X) -> X
        U11(tt()) -> tt()
        U21(tt(),V2) -> U22(isList(activate(V2)))
        U22(tt()) -> tt()
        U31(tt()) -> tt()
        U42(tt()) -> tt()
        U51(tt(),V2) -> U52(isList(activate(V2)))
        U52(tt()) -> tt()
        U61(tt()) -> tt()
        U72(tt()) -> tt()
        U81(tt()) -> tt()
        isList(n__nil()) -> tt()
        isPal(n__nil()) -> tt()
        isQid(n__a()) -> tt()
        isQid(n__e()) -> tt()
        isQid(n__i()) -> tt()
        isQid(n__o()) -> tt()
        isQid(n__u()) -> tt()
        __(X1,X2) -> n____(X1,X2)
        activate(n__nil()) -> nil()
        activate(n__a()) -> a()
        activate(n__e()) -> e()
        activate(n__i()) -> i()
        activate(n__o()) -> o()
        activate(n__u()) -> u()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [u] = 0,
         
         [o] = 3,
         
         [i] = 14,
         
         [e] = 8,
         
         [a] = 0,
         
         [n__u] = 0,
         
         [n__o] = 3,
         
         [n__i] = 14,
         
         [n__e] = 8,
         
         [n__a] = 0,
         
         [isNePal](x0) = x0 + 14,
         
         [isQid](x0) = x0 + 3,
         
         [n____](x0, x1) = x0 + x1,
         
         [n__nil] = 0,
         
         [U81](x0) = x0,
         
         [U72](x0) = x0,
         
         [isPal](x0) = x0 + 15,
         
         [U71](x0, x1) = x0 + x1 + 13,
         
         [U61](x0) = x0 + 9,
         
         [U52](x0) = x0,
         
         [U51](x0, x1) = x0 + x1 + 14,
         
         [U42](x0) = x0,
         
         [isNeList](x0) = x0 + 12,
         
         [U41](x0, x1) = x0 + x1,
         
         [U31](x0) = x0 + 12,
         
         [U22](x0) = x0 + 1,
         
         [isList](x0) = x0 + 12,
         
         [activate](x0) = x0,
         
         [U21](x0, x1) = x0 + x1 + 12,
         
         [U11](x0) = x0 + 14,
         
         [tt] = 2,
         
         [nil] = 0,
         
         [__](x0, x1) = x0 + x1
        orientation:
         __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
         
         U41(tt(),V2) = V2 + 2 >= V2 + 12 = U42(isNeList(activate(V2)))
         
         isList(V) = V + 12 >= V + 26 = U11(isNeList(activate(V)))
         
         isList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 24 = U21(isList(activate(V1)),activate(V2))
         
         isNeList(V) = V + 12 >= V + 15 = U31(isQid(activate(V)))
         
         isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 26 = U51(isNeList(activate(V1)),activate(V2))
         
         isNePal(V) = V + 14 >= V + 12 = U61(isQid(activate(V)))
         
         isNePal(n____(I,__(P,I))) = 2I + P + 14 >= I + P + 16 = U71(isQid(activate(I)),activate(P))
         
         isPal(V) = V + 15 >= V + 14 = U81(isNePal(activate(V)))
         
         U71(tt(),P) = P + 15 >= P + 15 = U72(isPal(activate(P)))
         
         isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U41(isList(activate(V1)),activate(V2))
         
         nil() = 0 >= 0 = n__nil()
         
         a() = 0 >= 0 = n__a()
         
         e() = 8 >= 8 = n__e()
         
         i() = 14 >= 14 = n__i()
         
         o() = 3 >= 3 = n__o()
         
         u() = 0 >= 0 = n__u()
         
         activate(n____(X1,X2)) = X1 + X2 >= X1 + X2 = __(X1,X2)
         
         __(X,nil()) = X >= X = X
         
         __(nil(),X) = X >= X = X
         
         U11(tt()) = 16 >= 2 = tt()
         
         U21(tt(),V2) = V2 + 14 >= V2 + 13 = U22(isList(activate(V2)))
         
         U22(tt()) = 3 >= 2 = tt()
         
         U31(tt()) = 14 >= 2 = tt()
         
         U42(tt()) = 2 >= 2 = tt()
         
         U51(tt(),V2) = V2 + 16 >= V2 + 12 = U52(isList(activate(V2)))
         
         U52(tt()) = 2 >= 2 = tt()
         
         U61(tt()) = 11 >= 2 = tt()
         
         U72(tt()) = 2 >= 2 = tt()
         
         U81(tt()) = 2 >= 2 = tt()
         
         isList(n__nil()) = 12 >= 2 = tt()
         
         isPal(n__nil()) = 15 >= 2 = tt()
         
         isQid(n__a()) = 3 >= 2 = tt()
         
         isQid(n__e()) = 11 >= 2 = tt()
         
         isQid(n__i()) = 17 >= 2 = tt()
         
         isQid(n__o()) = 6 >= 2 = tt()
         
         isQid(n__u()) = 3 >= 2 = tt()
         
         __(X1,X2) = X1 + X2 >= X1 + X2 = n____(X1,X2)
         
         activate(n__nil()) = 0 >= 0 = nil()
         
         activate(n__a()) = 0 >= 0 = a()
         
         activate(n__e()) = 8 >= 8 = e()
         
         activate(n__i()) = 14 >= 14 = i()
         
         activate(n__o()) = 3 >= 3 = o()
         
         activate(n__u()) = 0 >= 0 = u()
         
         activate(X) = X >= X = X
        problem:
         strict:
          __(__(X,Y),Z) -> __(X,__(Y,Z))
          U41(tt(),V2) -> U42(isNeList(activate(V2)))
          isList(V) -> U11(isNeList(activate(V)))
          isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
          isNeList(V) -> U31(isQid(activate(V)))
          isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
          isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
         weak:
          isNePal(V) -> U61(isQid(activate(V)))
          isPal(V) -> U81(isNePal(activate(V)))
          U71(tt(),P) -> U72(isPal(activate(P)))
          isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
          nil() -> n__nil()
          a() -> n__a()
          e() -> n__e()
          i() -> n__i()
          o() -> n__o()
          u() -> n__u()
          activate(n____(X1,X2)) -> __(X1,X2)
          __(X,nil()) -> X
          __(nil(),X) -> X
          U11(tt()) -> tt()
          U21(tt(),V2) -> U22(isList(activate(V2)))
          U22(tt()) -> tt()
          U31(tt()) -> tt()
          U42(tt()) -> tt()
          U51(tt(),V2) -> U52(isList(activate(V2)))
          U52(tt()) -> tt()
          U61(tt()) -> tt()
          U72(tt()) -> tt()
          U81(tt()) -> tt()
          isList(n__nil()) -> tt()
          isPal(n__nil()) -> tt()
          isQid(n__a()) -> tt()
          isQid(n__e()) -> tt()
          isQid(n__i()) -> tt()
          isQid(n__o()) -> tt()
          isQid(n__u()) -> tt()
          __(X1,X2) -> n____(X1,X2)
          activate(n__nil()) -> nil()
          activate(n__a()) -> a()
          activate(n__e()) -> e()
          activate(n__i()) -> i()
          activate(n__o()) -> o()
          activate(n__u()) -> u()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [u] = 2,
           
           [o] = 9,
           
           [i] = 2,
           
           [e] = 4,
           
           [a] = 8,
           
           [n__u] = 2,
           
           [n__o] = 9,
           
           [n__i] = 2,
           
           [n__e] = 4,
           
           [n__a] = 8,
           
           [isNePal](x0) = x0,
           
           [isQid](x0) = x0,
           
           [n____](x0, x1) = x0 + x1,
           
           [n__nil] = 0,
           
           [U81](x0) = x0 + 4,
           
           [U72](x0) = x0 + 3,
           
           [isPal](x0) = x0 + 4,
           
           [U71](x0, x1) = x0 + x1 + 6,
           
           [U61](x0) = x0,
           
           [U52](x0) = x0,
           
           [U51](x0, x1) = x0 + x1 + 11,
           
           [U42](x0) = x0 + 3,
           
           [isNeList](x0) = x0 + 12,
           
           [U41](x0, x1) = x0 + x1,
           
           [U31](x0) = x0 + 5,
           
           [U22](x0) = x0 + 4,
           
           [isList](x0) = x0 + 12,
           
           [activate](x0) = x0,
           
           [U21](x0, x1) = x0 + x1 + 15,
           
           [U11](x0) = x0 + 5,
           
           [tt] = 1,
           
           [nil] = 0,
           
           [__](x0, x1) = x0 + x1
          orientation:
           __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
           
           U41(tt(),V2) = V2 + 1 >= V2 + 15 = U42(isNeList(activate(V2)))
           
           isList(V) = V + 12 >= V + 17 = U11(isNeList(activate(V)))
           
           isList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 27 = U21(isList(activate(V1)),activate(V2))
           
           isNeList(V) = V + 12 >= V + 5 = U31(isQid(activate(V)))
           
           isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 23 = U51(isNeList(activate(V1)),activate(V2))
           
           isNePal(n____(I,__(P,I))) = 2I + P >= I + P + 6 = U71(isQid(activate(I)),activate(P))
           
           isNePal(V) = V >= V = U61(isQid(activate(V)))
           
           isPal(V) = V + 4 >= V + 4 = U81(isNePal(activate(V)))
           
           U71(tt(),P) = P + 7 >= P + 7 = U72(isPal(activate(P)))
           
           isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U41(isList(activate(V1)),activate(V2))
           
           nil() = 0 >= 0 = n__nil()
           
           a() = 8 >= 8 = n__a()
           
           e() = 4 >= 4 = n__e()
           
           i() = 2 >= 2 = n__i()
           
           o() = 9 >= 9 = n__o()
           
           u() = 2 >= 2 = n__u()
           
           activate(n____(X1,X2)) = X1 + X2 >= X1 + X2 = __(X1,X2)
           
           __(X,nil()) = X >= X = X
           
           __(nil(),X) = X >= X = X
           
           U11(tt()) = 6 >= 1 = tt()
           
           U21(tt(),V2) = V2 + 16 >= V2 + 16 = U22(isList(activate(V2)))
           
           U22(tt()) = 5 >= 1 = tt()
           
           U31(tt()) = 6 >= 1 = tt()
           
           U42(tt()) = 4 >= 1 = tt()
           
           U51(tt(),V2) = V2 + 12 >= V2 + 12 = U52(isList(activate(V2)))
           
           U52(tt()) = 1 >= 1 = tt()
           
           U61(tt()) = 1 >= 1 = tt()
           
           U72(tt()) = 4 >= 1 = tt()
           
           U81(tt()) = 5 >= 1 = tt()
           
           isList(n__nil()) = 12 >= 1 = tt()
           
           isPal(n__nil()) = 4 >= 1 = tt()
           
           isQid(n__a()) = 8 >= 1 = tt()
           
           isQid(n__e()) = 4 >= 1 = tt()
           
           isQid(n__i()) = 2 >= 1 = tt()
           
           isQid(n__o()) = 9 >= 1 = tt()
           
           isQid(n__u()) = 2 >= 1 = tt()
           
           __(X1,X2) = X1 + X2 >= X1 + X2 = n____(X1,X2)
           
           activate(n__nil()) = 0 >= 0 = nil()
           
           activate(n__a()) = 8 >= 8 = a()
           
           activate(n__e()) = 4 >= 4 = e()
           
           activate(n__i()) = 2 >= 2 = i()
           
           activate(n__o()) = 9 >= 9 = o()
           
           activate(n__u()) = 2 >= 2 = u()
           
           activate(X) = X >= X = X
          problem:
           strict:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
           weak:
            isNeList(V) -> U31(isQid(activate(V)))
            isNePal(V) -> U61(isQid(activate(V)))
            isPal(V) -> U81(isNePal(activate(V)))
            U71(tt(),P) -> U72(isPal(activate(P)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            nil() -> n__nil()
            a() -> n__a()
            e() -> n__e()
            i() -> n__i()
            o() -> n__o()
            u() -> n__u()
            activate(n____(X1,X2)) -> __(X1,X2)
            __(X,nil()) -> X
            __(nil(),X) -> X
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            isList(n__nil()) -> tt()
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            __(X1,X2) -> n____(X1,X2)
            activate(n__nil()) -> nil()
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [u] = 7,
             
             [o] = 15,
             
             [i] = 0,
             
             [e] = 18,
             
             [a] = 1,
             
             [n__u] = 7,
             
             [n__o] = 15,
             
             [n__i] = 0,
             
             [n__e] = 18,
             
             [n__a] = 1,
             
             [isNePal](x0) = x0 + 4,
             
             [isQid](x0) = x0 + 1,
             
             [n____](x0, x1) = x0 + x1 + 27,
             
             [n__nil] = 0,
             
             [U81](x0) = x0 + 10,
             
             [U72](x0) = x0 + 9,
             
             [isPal](x0) = x0 + 15,
             
             [U71](x0, x1) = x0 + x1 + 25,
             
             [U61](x0) = x0,
             
             [U52](x0) = x0,
             
             [U51](x0, x1) = x0 + x1 + 16,
             
             [U42](x0) = x0 + 4,
             
             [isNeList](x0) = x0 + 8,
             
             [U41](x0, x1) = x0 + x1 + 28,
             
             [U31](x0) = x0 + 6,
             
             [U22](x0) = x0 + 18,
             
             [isList](x0) = x0 + 4,
             
             [activate](x0) = x0 + 1,
             
             [U21](x0, x1) = x0 + x1 + 23,
             
             [U11](x0) = x0 + 1,
             
             [tt] = 0,
             
             [nil] = 1,
             
             [__](x0, x1) = x0 + x1 + 28
            orientation:
             __(__(X,Y),Z) = X + Y + Z + 56 >= X + Y + Z + 56 = __(X,__(Y,Z))
             
             U41(tt(),V2) = V2 + 28 >= V2 + 13 = U42(isNeList(activate(V2)))
             
             isList(V) = V + 4 >= V + 10 = U11(isNeList(activate(V)))
             
             isList(n____(V1,V2)) = V1 + V2 + 31 >= V1 + V2 + 29 = U21(isList(activate(V1)),activate(V2))
             
             isNeList(n____(V1,V2)) = V1 + V2 + 35 >= V1 + V2 + 26 = U51(isNeList(activate(V1)),activate(V2))
             
             isNePal(n____(I,__(P,I))) = 2I + P + 59 >= I + P + 28 = U71(isQid(activate(I)),activate(P))
             
             isNeList(V) = V + 8 >= V + 8 = U31(isQid(activate(V)))
             
             isNePal(V) = V + 4 >= V + 2 = U61(isQid(activate(V)))
             
             isPal(V) = V + 15 >= V + 15 = U81(isNePal(activate(V)))
             
             U71(tt(),P) = P + 25 >= P + 25 = U72(isPal(activate(P)))
             
             isNeList(n____(V1,V2)) = V1 + V2 + 35 >= V1 + V2 + 34 = U41(isList(activate(V1)),activate(V2))
             
             nil() = 1 >= 0 = n__nil()
             
             a() = 1 >= 1 = n__a()
             
             e() = 18 >= 18 = n__e()
             
             i() = 0 >= 0 = n__i()
             
             o() = 15 >= 15 = n__o()
             
             u() = 7 >= 7 = n__u()
             
             activate(n____(X1,X2)) = X1 + X2 + 28 >= X1 + X2 + 28 = __(X1,X2)
             
             __(X,nil()) = X + 29 >= X = X
             
             __(nil(),X) = X + 29 >= X = X
             
             U11(tt()) = 1 >= 0 = tt()
             
             U21(tt(),V2) = V2 + 23 >= V2 + 23 = U22(isList(activate(V2)))
             
             U22(tt()) = 18 >= 0 = tt()
             
             U31(tt()) = 6 >= 0 = tt()
             
             U42(tt()) = 4 >= 0 = tt()
             
             U51(tt(),V2) = V2 + 16 >= V2 + 5 = U52(isList(activate(V2)))
             
             U52(tt()) = 0 >= 0 = tt()
             
             U61(tt()) = 0 >= 0 = tt()
             
             U72(tt()) = 9 >= 0 = tt()
             
             U81(tt()) = 10 >= 0 = tt()
             
             isList(n__nil()) = 4 >= 0 = tt()
             
             isPal(n__nil()) = 15 >= 0 = tt()
             
             isQid(n__a()) = 2 >= 0 = tt()
             
             isQid(n__e()) = 19 >= 0 = tt()
             
             isQid(n__i()) = 1 >= 0 = tt()
             
             isQid(n__o()) = 16 >= 0 = tt()
             
             isQid(n__u()) = 8 >= 0 = tt()
             
             __(X1,X2) = X1 + X2 + 28 >= X1 + X2 + 27 = n____(X1,X2)
             
             activate(n__nil()) = 1 >= 1 = nil()
             
             activate(n__a()) = 2 >= 1 = a()
             
             activate(n__e()) = 19 >= 18 = e()
             
             activate(n__i()) = 1 >= 0 = i()
             
             activate(n__o()) = 16 >= 15 = o()
             
             activate(n__u()) = 8 >= 7 = u()
             
             activate(X) = X + 1 >= X = X
            problem:
             strict:
              __(__(X,Y),Z) -> __(X,__(Y,Z))
              isList(V) -> U11(isNeList(activate(V)))
             weak:
              U41(tt(),V2) -> U42(isNeList(activate(V2)))
              isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
              isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
              isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
              isNeList(V) -> U31(isQid(activate(V)))
              isNePal(V) -> U61(isQid(activate(V)))
              isPal(V) -> U81(isNePal(activate(V)))
              U71(tt(),P) -> U72(isPal(activate(P)))
              isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
              nil() -> n__nil()
              a() -> n__a()
              e() -> n__e()
              i() -> n__i()
              o() -> n__o()
              u() -> n__u()
              activate(n____(X1,X2)) -> __(X1,X2)
              __(X,nil()) -> X
              __(nil(),X) -> X
              U11(tt()) -> tt()
              U21(tt(),V2) -> U22(isList(activate(V2)))
              U22(tt()) -> tt()
              U31(tt()) -> tt()
              U42(tt()) -> tt()
              U51(tt(),V2) -> U52(isList(activate(V2)))
              U52(tt()) -> tt()
              U61(tt()) -> tt()
              U72(tt()) -> tt()
              U81(tt()) -> tt()
              isList(n__nil()) -> tt()
              isPal(n__nil()) -> tt()
              isQid(n__a()) -> tt()
              isQid(n__e()) -> tt()
              isQid(n__i()) -> tt()
              isQid(n__o()) -> tt()
              isQid(n__u()) -> tt()
              __(X1,X2) -> n____(X1,X2)
              activate(n__nil()) -> nil()
              activate(n__a()) -> a()
              activate(n__e()) -> e()
              activate(n__i()) -> i()
              activate(n__o()) -> o()
              activate(n__u()) -> u()
              activate(X) -> X
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [u] = 2,
               
               [o] = 2,
               
               [i] = 5,
               
               [e] = 4,
               
               [a] = 11,
               
               [n__u] = 2,
               
               [n__o] = 2,
               
               [n__i] = 5,
               
               [n__e] = 4,
               
               [n__a] = 11,
               
               [isNePal](x0) = x0 + 10,
               
               [isQid](x0) = x0 + 10,
               
               [n____](x0, x1) = x0 + x1 + 1,
               
               [n__nil] = 14,
               
               [U81](x0) = x0 + 2,
               
               [U72](x0) = x0 + 2,
               
               [isPal](x0) = x0 + 12,
               
               [U71](x0, x1) = x0 + x1 + 2,
               
               [U61](x0) = x0,
               
               [U52](x0) = x0 + 2,
               
               [U51](x0, x1) = x0 + x1 + 1,
               
               [U42](x0) = x0 + 2,
               
               [isNeList](x0) = x0 + 10,
               
               [U41](x0, x1) = x0 + x1,
               
               [U31](x0) = x0,
               
               [U22](x0) = x0 + 2,
               
               [isList](x0) = x0 + 11,
               
               [activate](x0) = x0,
               
               [U21](x0, x1) = x0 + x1 + 1,
               
               [U11](x0) = x0,
               
               [tt] = 12,
               
               [nil] = 14,
               
               [__](x0, x1) = x0 + x1 + 1
              orientation:
               __(__(X,Y),Z) = X + Y + Z + 2 >= X + Y + Z + 2 = __(X,__(Y,Z))
               
               isList(V) = V + 11 >= V + 10 = U11(isNeList(activate(V)))
               
               U41(tt(),V2) = V2 + 12 >= V2 + 12 = U42(isNeList(activate(V2)))
               
               isList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U21(isList(activate(V1)),activate(V2))
               
               isNeList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 11 = U51(isNeList(activate(V1)),activate(V2))
               
               isNePal(n____(I,__(P,I))) = 2I + P + 12 >= I + P + 12 = U71(isQid(activate(I)),activate(P))
               
               isNeList(V) = V + 10 >= V + 10 = U31(isQid(activate(V)))
               
               isNePal(V) = V + 10 >= V + 10 = U61(isQid(activate(V)))
               
               isPal(V) = V + 12 >= V + 12 = U81(isNePal(activate(V)))
               
               U71(tt(),P) = P + 14 >= P + 14 = U72(isPal(activate(P)))
               
               isNeList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 11 = U41(isList(activate(V1)),activate(V2))
               
               nil() = 14 >= 14 = n__nil()
               
               a() = 11 >= 11 = n__a()
               
               e() = 4 >= 4 = n__e()
               
               i() = 5 >= 5 = n__i()
               
               o() = 2 >= 2 = n__o()
               
               u() = 2 >= 2 = n__u()
               
               activate(n____(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = __(X1,X2)
               
               __(X,nil()) = X + 15 >= X = X
               
               __(nil(),X) = X + 15 >= X = X
               
               U11(tt()) = 12 >= 12 = tt()
               
               U21(tt(),V2) = V2 + 13 >= V2 + 13 = U22(isList(activate(V2)))
               
               U22(tt()) = 14 >= 12 = tt()
               
               U31(tt()) = 12 >= 12 = tt()
               
               U42(tt()) = 14 >= 12 = tt()
               
               U51(tt(),V2) = V2 + 13 >= V2 + 13 = U52(isList(activate(V2)))
               
               U52(tt()) = 14 >= 12 = tt()
               
               U61(tt()) = 12 >= 12 = tt()
               
               U72(tt()) = 14 >= 12 = tt()
               
               U81(tt()) = 14 >= 12 = tt()
               
               isList(n__nil()) = 25 >= 12 = tt()
               
               isPal(n__nil()) = 26 >= 12 = tt()
               
               isQid(n__a()) = 21 >= 12 = tt()
               
               isQid(n__e()) = 14 >= 12 = tt()
               
               isQid(n__i()) = 15 >= 12 = tt()
               
               isQid(n__o()) = 12 >= 12 = tt()
               
               isQid(n__u()) = 12 >= 12 = tt()
               
               __(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 1 = n____(X1,X2)
               
               activate(n__nil()) = 14 >= 14 = nil()
               
               activate(n__a()) = 11 >= 11 = a()
               
               activate(n__e()) = 4 >= 4 = e()
               
               activate(n__i()) = 5 >= 5 = i()
               
               activate(n__o()) = 2 >= 2 = o()
               
               activate(n__u()) = 2 >= 2 = u()
               
               activate(X) = X >= X = X
              problem:
               strict:
                __(__(X,Y),Z) -> __(X,__(Y,Z))
               weak:
                isList(V) -> U11(isNeList(activate(V)))
                U41(tt(),V2) -> U42(isNeList(activate(V2)))
                isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                isNeList(V) -> U31(isQid(activate(V)))
                isNePal(V) -> U61(isQid(activate(V)))
                isPal(V) -> U81(isNePal(activate(V)))
                U71(tt(),P) -> U72(isPal(activate(P)))
                isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                nil() -> n__nil()
                a() -> n__a()
                e() -> n__e()
                i() -> n__i()
                o() -> n__o()
                u() -> n__u()
                activate(n____(X1,X2)) -> __(X1,X2)
                __(X,nil()) -> X
                __(nil(),X) -> X
                U11(tt()) -> tt()
                U21(tt(),V2) -> U22(isList(activate(V2)))
                U22(tt()) -> tt()
                U31(tt()) -> tt()
                U42(tt()) -> tt()
                U51(tt(),V2) -> U52(isList(activate(V2)))
                U52(tt()) -> tt()
                U61(tt()) -> tt()
                U72(tt()) -> tt()
                U81(tt()) -> tt()
                isList(n__nil()) -> tt()
                isPal(n__nil()) -> tt()
                isQid(n__a()) -> tt()
                isQid(n__e()) -> tt()
                isQid(n__i()) -> tt()
                isQid(n__o()) -> tt()
                isQid(n__u()) -> tt()
                __(X1,X2) -> n____(X1,X2)
                activate(n__nil()) -> nil()
                activate(n__a()) -> a()
                activate(n__e()) -> e()
                activate(n__i()) -> i()
                activate(n__o()) -> o()
                activate(n__u()) -> u()
                activate(X) -> X
              Matrix Interpretation Processor:
               dimension: 2
               max_matrix:
                [1 2]
                [0 1]
                interpretation:
                       [2]
                 [u] = [0],
                 
                       [1]
                 [o] = [0],
                 
                       [1]
                 [i] = [0],
                 
                       [1]
                 [e] = [3],
                 
                       [1]
                 [a] = [2],
                 
                          [2]
                 [n__u] = [0],
                 
                          [1]
                 [n__o] = [0],
                 
                          [1]
                 [n__i] = [0],
                 
                          [1]
                 [n__e] = [3],
                 
                          [1]
                 [n__a] = [2],
                 
                                 [1 2]     [0]
                 [isNePal](x0) = [0 0]x0 + [3],
                 
                               [1 0]  
                 [isQid](x0) = [0 0]x0,
                 
                                   [1 2]          [1]
                 [n____](x0, x1) = [0 1]x0 + x1 + [3],
                 
                            [1]
                 [n__nil] = [0],
                 
                             [1 0]     [1]
                 [U81](x0) = [0 0]x0 + [0],
                 
                             [1 0]  
                 [U72](x0) = [0 0]x0,
                 
                               [1 2]     [1]
                 [isPal](x0) = [0 0]x0 + [1],
                 
                                 [1 0]     [1 2]  
                 [U71](x0, x1) = [0 0]x0 + [0 0]x1,
                 
                             [1 0]     [0]
                 [U61](x0) = [0 0]x0 + [2],
                 
                             [1 0]     [1]
                 [U52](x0) = [0 0]x0 + [0],
                 
                                 [1 0]     [1 0]     [0]
                 [U51](x0, x1) = [0 0]x0 + [0 0]x1 + [1],
                 
                             [1 1]     [0]
                 [U42](x0) = [0 0]x0 + [1],
                 
                                  [1 0]     [0]
                 [isNeList](x0) = [0 0]x0 + [1],
                 
                                 [1 0]     [1 0]     [0]
                 [U41](x0, x1) = [0 0]x0 + [0 0]x1 + [1],
                 
                             [1 0]  
                 [U31](x0) = [0 0]x0,
                 
                             [1 0]     [1]
                 [U22](x0) = [0 0]x0 + [0],
                 
                                     [0]
                 [isList](x0) = x0 + [1],
                 
                                    
                 [activate](x0) = x0,
                 
                                 [1 1]     [1 0]  
                 [U21](x0, x1) = [0 1]x0 + [0 0]x1,
                 
                             [1 0]     [0]
                 [U11](x0) = [0 0]x0 + [1],
                 
                        [1]
                 [tt] = [0],
                 
                         [1]
                 [nil] = [0],
                 
                                [1 2]          [1]
                 [__](x0, x1) = [0 1]x0 + x1 + [3]
                orientation:
                                 [1 4]    [1 2]        [8]    [1 2]    [1 2]        [2]                
                 __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [6] >= [0 1]X + [0 1]Y + Z + [6] = __(X,__(Y,Z))
                 
                                 [0]    [1 0]    [0]                             
                 isList(V) = V + [1] >= [0 0]V + [1] = U11(isNeList(activate(V)))
                 
                                [1 0]     [1]    [1 0]     [1]                              
                 U41(tt(),V2) = [0 0]V2 + [1] >= [0 0]V2 + [1] = U42(isNeList(activate(V2)))
                 
                                        [1 2]          [1]    [1 1]     [1 0]     [1]                                         
                 isList(n____(V1,V2)) = [0 1]V1 + V2 + [4] >= [0 1]V1 + [0 0]V2 + [1] = U21(isList(activate(V1)),activate(V2))
                 
                                          [1 2]     [1 0]     [1]    [1 0]     [1 0]     [0]                                           
                 isNeList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 + [1] >= [0 0]V1 + [0 0]V2 + [1] = U51(isNeList(activate(V1)),activate(V2))
                 
                                             [2 6]    [1 4]    [14]    [1 0]    [1 2]                                       
                 isNePal(n____(I,__(P,I))) = [0 0]I + [0 0]P + [3 ] >= [0 0]I + [0 0]P = U71(isQid(activate(I)),activate(P))
                 
                               [1 0]    [0]    [1 0]                           
                 isNeList(V) = [0 0]V + [1] >= [0 0]V = U31(isQid(activate(V)))
                 
                              [1 2]    [0]    [1 0]    [0]                          
                 isNePal(V) = [0 0]V + [3] >= [0 0]V + [2] = U61(isQid(activate(V)))
                 
                            [1 2]    [1]    [1 2]    [1]                            
                 isPal(V) = [0 0]V + [1] >= [0 0]V + [0] = U81(isNePal(activate(V)))
                 
                               [1 2]    [1]    [1 2]    [1]                          
                 U71(tt(),P) = [0 0]P + [0] >= [0 0]P + [0] = U72(isPal(activate(P)))
                 
                                          [1 2]     [1 0]     [1]    [1 0]     [1 0]     [0]                                         
                 isNeList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 + [1] >= [0 0]V1 + [0 0]V2 + [1] = U41(isList(activate(V1)),activate(V2))
                 
                         [1]    [1]           
                 nil() = [0] >= [0] = n__nil()
                 
                       [1]    [1]         
                 a() = [2] >= [2] = n__a()
                 
                       [1]    [1]         
                 e() = [3] >= [3] = n__e()
                 
                       [1]    [1]         
                 i() = [0] >= [0] = n__i()
                 
                       [1]    [1]         
                 o() = [0] >= [0] = n__o()
                 
                       [2]    [2]         
                 u() = [0] >= [0] = n__u()
                 
                                          [1 2]          [1]    [1 2]          [1]            
                 activate(n____(X1,X2)) = [0 1]X1 + X2 + [3] >= [0 1]X1 + X2 + [3] = __(X1,X2)
                 
                               [1 2]    [2]         
                 __(X,nil()) = [0 1]X + [3] >= X = X
                 
                                   [2]         
                 __(nil(),X) = X + [3] >= X = X
                 
                             [1]    [1]       
                 U11(tt()) = [1] >= [0] = tt()
                 
                                [1 0]     [1]    [1 0]     [1]                            
                 U21(tt(),V2) = [0 0]V2 + [0] >= [0 0]V2 + [0] = U22(isList(activate(V2)))
                 
                             [2]    [1]       
                 U22(tt()) = [0] >= [0] = tt()
                 
                             [1]    [1]       
                 U31(tt()) = [0] >= [0] = tt()
                 
                             [1]    [1]       
                 U42(tt()) = [1] >= [0] = tt()
                 
                                [1 0]     [1]    [1 0]     [1]                            
                 U51(tt(),V2) = [0 0]V2 + [1] >= [0 0]V2 + [0] = U52(isList(activate(V2)))
                 
                             [2]    [1]       
                 U52(tt()) = [0] >= [0] = tt()
                 
                             [1]    [1]       
                 U61(tt()) = [2] >= [0] = tt()
                 
                             [1]    [1]       
                 U72(tt()) = [0] >= [0] = tt()
                 
                             [2]    [1]       
                 U81(tt()) = [0] >= [0] = tt()
                 
                                    [1]    [1]       
                 isList(n__nil()) = [1] >= [0] = tt()
                 
                                   [2]    [1]       
                 isPal(n__nil()) = [1] >= [0] = tt()
                 
                                 [1]    [1]       
                 isQid(n__a()) = [0] >= [0] = tt()
                 
                                 [1]    [1]       
                 isQid(n__e()) = [0] >= [0] = tt()
                 
                                 [1]    [1]       
                 isQid(n__i()) = [0] >= [0] = tt()
                 
                                 [1]    [1]       
                 isQid(n__o()) = [0] >= [0] = tt()
                 
                                 [2]    [1]       
                 isQid(n__u()) = [0] >= [0] = tt()
                 
                             [1 2]          [1]    [1 2]          [1]               
                 __(X1,X2) = [0 1]X1 + X2 + [3] >= [0 1]X1 + X2 + [3] = n____(X1,X2)
                 
                                      [1]    [1]        
                 activate(n__nil()) = [0] >= [0] = nil()
                 
                                    [1]    [1]      
                 activate(n__a()) = [2] >= [2] = a()
                 
                                    [1]    [1]      
                 activate(n__e()) = [3] >= [3] = e()
                 
                                    [1]    [1]      
                 activate(n__i()) = [0] >= [0] = i()
                 
                                    [1]    [1]      
                 activate(n__o()) = [0] >= [0] = o()
                 
                                    [2]    [2]      
                 activate(n__u()) = [0] >= [0] = u()
                 
                                         
                 activate(X) = X >= X = X
                problem:
                 strict:
                  
                 weak:
                  __(__(X,Y),Z) -> __(X,__(Y,Z))
                  isList(V) -> U11(isNeList(activate(V)))
                  U41(tt(),V2) -> U42(isNeList(activate(V2)))
                  isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                  isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                  isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                  isNeList(V) -> U31(isQid(activate(V)))
                  isNePal(V) -> U61(isQid(activate(V)))
                  isPal(V) -> U81(isNePal(activate(V)))
                  U71(tt(),P) -> U72(isPal(activate(P)))
                  isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                  nil() -> n__nil()
                  a() -> n__a()
                  e() -> n__e()
                  i() -> n__i()
                  o() -> n__o()
                  u() -> n__u()
                  activate(n____(X1,X2)) -> __(X1,X2)
                  __(X,nil()) -> X
                  __(nil(),X) -> X
                  U11(tt()) -> tt()
                  U21(tt(),V2) -> U22(isList(activate(V2)))
                  U22(tt()) -> tt()
                  U31(tt()) -> tt()
                  U42(tt()) -> tt()
                  U51(tt(),V2) -> U52(isList(activate(V2)))
                  U52(tt()) -> tt()
                  U61(tt()) -> tt()
                  U72(tt()) -> tt()
                  U81(tt()) -> tt()
                  isList(n__nil()) -> tt()
                  isPal(n__nil()) -> tt()
                  isQid(n__a()) -> tt()
                  isQid(n__e()) -> tt()
                  isQid(n__i()) -> tt()
                  isQid(n__o()) -> tt()
                  isQid(n__u()) -> tt()
                  __(X1,X2) -> n____(X1,X2)
                  activate(n__nil()) -> nil()
                  activate(n__a()) -> a()
                  activate(n__e()) -> e()
                  activate(n__i()) -> i()
                  activate(n__o()) -> o()
                  activate(n__u()) -> u()
                  activate(X) -> X
                Qed